package fos

import scala.util.parsing.combinator.syntactical.StandardTokenParsers
import scala.util.parsing.input._
import scala.util.parsing.syntax._

/** This object implements a parser and evaluator for the
 *  untyped lambda calculus found in Chapter 5 of
 *  the TAPL book.
 *  @author Jessa Bekker
 *  @author Nicolas Stucki
 */
object Untyped extends StandardTokenParsers {
  import lexical.Identifier
  lexical.delimiters ++= List("(", ")", "\\", ".")

  /**
   * Parser for t (but refactored into levels):
   * t:=   x
   * 	 | "\" x "." t
   * 	 | t t
   * 	 | "(" t ")"
   * 
   * the refactorization yeilds: t := tl1
   */
  def TermExp: Parser[Term] = (
      TermExpLevel1
    | failure("illegal start of term")
  )
  
  /**
   * Parser for tl1:
   * tl1 := tl2 (tl2)*
   */
  def TermExpLevel1: Parser[Term] = (
      rep1(TermExpLevel2) ^^ { case h::tail => (h /: tail) (Application(_,_)); case Nil/*this will never happen*/ => null }
  )
  
  /**
   * Parser for tl2:
   * tl2 :=   x
   * 	 	| "\" x "." tl1
   * 	 	| "(" tl1 ")"
   */
  def TermExpLevel2: Parser[Term] = (
      ident ^^ { case v => Variable(v) }
    | ("\\" ~> ident) ~ ("." ~> TermExpLevel1) ^^ { case v ~ t => Abstraction(Variable(v),t) }
    | "(" ~> TermExpLevel1 <~ ")" ^^ { case t => t }
  )
   
  
  /** Term 't' does not match any reduction rule. */
  case class NoRuleApplies(t: Term) extends Exception(t.toString)

  def alpha(t: Term, y: Variable): Term = t match{
    case `y` => Variable(y.name+"$")
    case v: Variable => v
    case Abstraction(`y`,t) => Abstraction(Variable(y.name+"$"), subst(t,y,Variable(y.name+"$"))) 
    case Abstraction(x,t) => Abstraction(x, alpha(t,y)) 
    case Application(t1,t2)=> Application(alpha(t1,y), alpha(t2,y))
  }
  
  def subst(t: Term, x: Variable, s: Term): Term = t match{
    case `x` => s
    case v: Variable => v
    case Abstraction(`x`, t1) => Abstraction(x, t1)
    case Abstraction(y,t1) => if (y isInFreeVarsOf s) subst(alpha(t,y),x,s) else Abstraction(y, subst(t1, x, s))
    case Application(t1,t2) => Application(subst(t1,x,s), subst(t2,x,s))
  }
  
  def isInFreeVarsOf(y:Variable, s:Term): Boolean = s match{
    case `y`  => true
    case Variable(_) => false
    case Abstraction(`y`,_) => false
    case Abstraction(_,t) => isInFreeVarsOf(y,t)
    case Application(t1,t2) => isInFreeVarsOf(y,t1) || isInFreeVarsOf(y,t2) 
  }
  
  /** Normal order (leftmost, outermost redex first).
   *
   *  @param t the initial term
   *  @return  the reduced term
   */
  def reduceNormalOrder(t: Term): Term = t match {
    case Abstraction(x,t) => Abstraction(x,reduceNormalOrder(t)) 
    case Application(Abstraction(x, t1), t2) => subst(t1, x, t2)
    case Application(t1,t2) => Application(reduceNormalOrder(t1),t2)
    case noRA: NoRuleApplies => noRA
    case _ => throw NoRuleApplies(t)
  }
  
  /** Call by value reducer. */
  def reduceCallByValue(t: Term): Term = t match {
  	case Application(Abstraction(x, t1), t2: Abstraction) => subst(t1, x, t2) // Only apply substitution if t2 is an abstraction
  	case Application(t1,t2) => Application(reduceCallByValue(t1),t2)
    case noRA: NoRuleApplies => noRA
    case _ => throw NoRuleApplies(t)
  }

  /** Returns a stream of terms, each being one step of reduction.
   *
   *  @param t      the initial term
   *  @param reduce the method that reduces a term by one step.
   *  @return       the stream of terms representing the big reduction.
   */
  def path(t: Term, reduce: Term => Term): Stream[Term] = 
    try {
      var t1 = reduce(t)
      Stream.cons(t, path(t1, reduce))
    } catch {
      case NoRuleApplies(_) =>
        Stream.cons(t, Stream.empty)
    }

  def main(args: Array[String]): Unit = {
    print("input: ")
    
    val tokens = new lexical.Scanner(StreamReader(new java.io.InputStreamReader(System.in)))
    
    phrase(TermExp)(tokens) match {
      case Success(trees, _) =>
        
      	println("normal order: ")
        for (t <- path(trees, reduceNormalOrder))
          println(t)
        println("call-by-value: ")

        for (t <- path(trees, reduceCallByValue))
          println(t)

      case e =>
        println(e)
    } 
    println
  }
}
